(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun p () String)
(declare-fun e () String)
(declare-fun f () String)
(declare-fun q () String)
(declare-fun g () String)
(declare-fun h () String)
(declare-fun i () String)
(declare-fun j () String)
(declare-fun k () String)
(declare-fun l () Bool)
(declare-fun m () Bool)
(declare-fun n () Bool)
(declare-fun o () String)
(assert (ite m (and (= c a) (= o e) (not (ite n (and (= d b) (= q k) (not (str.in_re i (re.++ (str.to_re "m") (re.range "6" "7"))))) (= f "")))) (str.in_re h (str.to_re (ite (= o (str.++ p f)) "2" j)))))
(assert (ite n (and (= f (ite l (ite (= a 0) g e) "9")) (not (str.in_re i (re.++ (str.to_re (ite (= c 1) "." "b")) (str.to_re "="))))) false))
(assert (not (= f "6")))
(check-sat)
